(0) Obligation:
Clauses:
p(s(0), 0).
p(s(s(X)), s(s(Y))) :- p(s(X), s(Y)).
plus(0, Y, Y).
plus(s(X), Y, s(Z)) :- ','(p(s(X), U), plus(U, Y, Z)).
Query: plus(g,a,a)
(1) PrologToDTProblemTransformerProof (SOUND transformation)
Built DT problem from termination graph DT10.
(2) Obligation:
Triples:
pB(s(X1), s(X2)) :- pB(X1, X2).
plusA(s(s(X1)), X2, s(X3)) :- pB(X1, X4).
plusA(s(s(X1)), X2, s(X3)) :- ','(pcB(X1, X4), plusA(s(s(X4)), X2, X3)).
Clauses:
pluscA(0, X1, X1).
pluscA(s(0), X1, s(X1)).
pluscA(s(s(X1)), X2, s(X3)) :- ','(pcB(X1, X4), pluscA(s(s(X4)), X2, X3)).
pcB(s(X1), s(X2)) :- pcB(X1, X2).
Afs:
plusA(x1, x2, x3) = plusA(x1)
(3) TriplesToPiDPProof (SOUND transformation)
We use the technique of [DT09]. With regard to the inferred argument filtering the predicates were used in the following modes:
plusA_in: (b,f,f)
pB_in: (b,f)
pcB_in: (b,f)
Transforming
TRIPLES into the following
Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:
PLUSA_IN_GAA(s(s(X1)), X2, s(X3)) → U2_GAA(X1, X2, X3, pB_in_ga(X1, X4))
PLUSA_IN_GAA(s(s(X1)), X2, s(X3)) → PB_IN_GA(X1, X4)
PB_IN_GA(s(X1), s(X2)) → U1_GA(X1, X2, pB_in_ga(X1, X2))
PB_IN_GA(s(X1), s(X2)) → PB_IN_GA(X1, X2)
PLUSA_IN_GAA(s(s(X1)), X2, s(X3)) → U3_GAA(X1, X2, X3, pcB_in_ga(X1, X4))
U3_GAA(X1, X2, X3, pcB_out_ga(X1, X4)) → U4_GAA(X1, X2, X3, plusA_in_gaa(s(s(X4)), X2, X3))
U3_GAA(X1, X2, X3, pcB_out_ga(X1, X4)) → PLUSA_IN_GAA(s(s(X4)), X2, X3)
The TRS R consists of the following rules:
pcB_in_ga(s(X1), s(X2)) → U8_ga(X1, X2, pcB_in_ga(X1, X2))
U8_ga(X1, X2, pcB_out_ga(X1, X2)) → pcB_out_ga(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
plusA_in_gaa(
x1,
x2,
x3) =
plusA_in_gaa(
x1)
s(
x1) =
s(
x1)
pB_in_ga(
x1,
x2) =
pB_in_ga(
x1)
pcB_in_ga(
x1,
x2) =
pcB_in_ga(
x1)
U8_ga(
x1,
x2,
x3) =
U8_ga(
x1,
x3)
pcB_out_ga(
x1,
x2) =
pcB_out_ga(
x1,
x2)
PLUSA_IN_GAA(
x1,
x2,
x3) =
PLUSA_IN_GAA(
x1)
U2_GAA(
x1,
x2,
x3,
x4) =
U2_GAA(
x1,
x4)
PB_IN_GA(
x1,
x2) =
PB_IN_GA(
x1)
U1_GA(
x1,
x2,
x3) =
U1_GA(
x1,
x3)
U3_GAA(
x1,
x2,
x3,
x4) =
U3_GAA(
x1,
x4)
U4_GAA(
x1,
x2,
x3,
x4) =
U4_GAA(
x1,
x4)
We have to consider all (P,R,Pi)-chains
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PLUSA_IN_GAA(s(s(X1)), X2, s(X3)) → U2_GAA(X1, X2, X3, pB_in_ga(X1, X4))
PLUSA_IN_GAA(s(s(X1)), X2, s(X3)) → PB_IN_GA(X1, X4)
PB_IN_GA(s(X1), s(X2)) → U1_GA(X1, X2, pB_in_ga(X1, X2))
PB_IN_GA(s(X1), s(X2)) → PB_IN_GA(X1, X2)
PLUSA_IN_GAA(s(s(X1)), X2, s(X3)) → U3_GAA(X1, X2, X3, pcB_in_ga(X1, X4))
U3_GAA(X1, X2, X3, pcB_out_ga(X1, X4)) → U4_GAA(X1, X2, X3, plusA_in_gaa(s(s(X4)), X2, X3))
U3_GAA(X1, X2, X3, pcB_out_ga(X1, X4)) → PLUSA_IN_GAA(s(s(X4)), X2, X3)
The TRS R consists of the following rules:
pcB_in_ga(s(X1), s(X2)) → U8_ga(X1, X2, pcB_in_ga(X1, X2))
U8_ga(X1, X2, pcB_out_ga(X1, X2)) → pcB_out_ga(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
plusA_in_gaa(
x1,
x2,
x3) =
plusA_in_gaa(
x1)
s(
x1) =
s(
x1)
pB_in_ga(
x1,
x2) =
pB_in_ga(
x1)
pcB_in_ga(
x1,
x2) =
pcB_in_ga(
x1)
U8_ga(
x1,
x2,
x3) =
U8_ga(
x1,
x3)
pcB_out_ga(
x1,
x2) =
pcB_out_ga(
x1,
x2)
PLUSA_IN_GAA(
x1,
x2,
x3) =
PLUSA_IN_GAA(
x1)
U2_GAA(
x1,
x2,
x3,
x4) =
U2_GAA(
x1,
x4)
PB_IN_GA(
x1,
x2) =
PB_IN_GA(
x1)
U1_GA(
x1,
x2,
x3) =
U1_GA(
x1,
x3)
U3_GAA(
x1,
x2,
x3,
x4) =
U3_GAA(
x1,
x4)
U4_GAA(
x1,
x2,
x3,
x4) =
U4_GAA(
x1,
x4)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 4 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PB_IN_GA(s(X1), s(X2)) → PB_IN_GA(X1, X2)
The TRS R consists of the following rules:
pcB_in_ga(s(X1), s(X2)) → U8_ga(X1, X2, pcB_in_ga(X1, X2))
U8_ga(X1, X2, pcB_out_ga(X1, X2)) → pcB_out_ga(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
pcB_in_ga(
x1,
x2) =
pcB_in_ga(
x1)
U8_ga(
x1,
x2,
x3) =
U8_ga(
x1,
x3)
pcB_out_ga(
x1,
x2) =
pcB_out_ga(
x1,
x2)
PB_IN_GA(
x1,
x2) =
PB_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PB_IN_GA(s(X1), s(X2)) → PB_IN_GA(X1, X2)
R is empty.
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
PB_IN_GA(
x1,
x2) =
PB_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PB_IN_GA(s(X1)) → PB_IN_GA(X1)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- PB_IN_GA(s(X1)) → PB_IN_GA(X1)
The graph contains the following edges 1 > 1
(13) YES
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
PLUSA_IN_GAA(s(s(X1)), X2, s(X3)) → U3_GAA(X1, X2, X3, pcB_in_ga(X1, X4))
U3_GAA(X1, X2, X3, pcB_out_ga(X1, X4)) → PLUSA_IN_GAA(s(s(X4)), X2, X3)
The TRS R consists of the following rules:
pcB_in_ga(s(X1), s(X2)) → U8_ga(X1, X2, pcB_in_ga(X1, X2))
U8_ga(X1, X2, pcB_out_ga(X1, X2)) → pcB_out_ga(s(X1), s(X2))
The argument filtering Pi contains the following mapping:
s(
x1) =
s(
x1)
pcB_in_ga(
x1,
x2) =
pcB_in_ga(
x1)
U8_ga(
x1,
x2,
x3) =
U8_ga(
x1,
x3)
pcB_out_ga(
x1,
x2) =
pcB_out_ga(
x1,
x2)
PLUSA_IN_GAA(
x1,
x2,
x3) =
PLUSA_IN_GAA(
x1)
U3_GAA(
x1,
x2,
x3,
x4) =
U3_GAA(
x1,
x4)
We have to consider all (P,R,Pi)-chains
(15) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
PLUSA_IN_GAA(s(s(X1))) → U3_GAA(X1, pcB_in_ga(X1))
U3_GAA(X1, pcB_out_ga(X1, X4)) → PLUSA_IN_GAA(s(s(X4)))
The TRS R consists of the following rules:
pcB_in_ga(s(X1)) → U8_ga(X1, pcB_in_ga(X1))
U8_ga(X1, pcB_out_ga(X1, X2)) → pcB_out_ga(s(X1), s(X2))
The set Q consists of the following terms:
pcB_in_ga(x0)
U8_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(17) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
PLUSA_IN_GAA(s(s(X1))) → U3_GAA(X1, pcB_in_ga(X1))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:
POL(PLUSA_IN_GAA(x1)) = 1 + x1
POL(U3_GAA(x1, x2)) = x2
POL(U8_ga(x1, x2)) = x2
POL(pcB_in_ga(x1)) = x1
POL(pcB_out_ga(x1, x2)) = 1 + x2
POL(s(x1)) = x1
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
pcB_in_ga(s(X1)) → U8_ga(X1, pcB_in_ga(X1))
U8_ga(X1, pcB_out_ga(X1, X2)) → pcB_out_ga(s(X1), s(X2))
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U3_GAA(X1, pcB_out_ga(X1, X4)) → PLUSA_IN_GAA(s(s(X4)))
The TRS R consists of the following rules:
pcB_in_ga(s(X1)) → U8_ga(X1, pcB_in_ga(X1))
U8_ga(X1, pcB_out_ga(X1, X2)) → pcB_out_ga(s(X1), s(X2))
The set Q consists of the following terms:
pcB_in_ga(x0)
U8_ga(x0, x1)
We have to consider all (P,Q,R)-chains.
(19) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(20) TRUE